Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a__from(X)  → cons(mark(X),from(s(X)))
2:    a__sel(0,cons(X,Y))  → mark(X)
3:    a__sel(s(X),cons(Y,Z))  → a__sel(mark(X),mark(Z))
4:    mark(from(X))  → a__from(mark(X))
5:    mark(sel(X1,X2))  → a__sel(mark(X1),mark(X2))
6:    mark(cons(X1,X2))  → cons(mark(X1),X2)
7:    mark(s(X))  → s(mark(X))
8:    mark(0)  → 0
9:    a__from(X)  → from(X)
10:    a__sel(X1,X2)  → sel(X1,X2)
There are 12 dependency pairs:
11:    A__FROM(X)  → MARK(X)
12:    A__SEL(0,cons(X,Y))  → MARK(X)
13:    A__SEL(s(X),cons(Y,Z))  → A__SEL(mark(X),mark(Z))
14:    A__SEL(s(X),cons(Y,Z))  → MARK(X)
15:    A__SEL(s(X),cons(Y,Z))  → MARK(Z)
16:    MARK(from(X))  → A__FROM(mark(X))
17:    MARK(from(X))  → MARK(X)
18:    MARK(sel(X1,X2))  → A__SEL(mark(X1),mark(X2))
19:    MARK(sel(X1,X2))  → MARK(X1)
20:    MARK(sel(X1,X2))  → MARK(X2)
21:    MARK(cons(X1,X2))  → MARK(X1)
22:    MARK(s(X))  → MARK(X)
Consider the SCC {11-22}. The constraints could not be solved.
Tyrolean Termination Tool  (0.28 seconds)   ---  May 3, 2006